Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		times(x,plus(y,s(z)))	→ plus(times(x,plus(y,times(s(z),0))),times(x,s(z)))
2:		times(x,0)	→ 0
3:		times(x,s(y))	→ plus(times(x,y),x)
4:		plus(x,0)	→ x
5:		plus(x,s(y))	→ s(plus(x,y))

There are 8 dependency pairs:


6:		TIMES(x,plus(y,s(z)))	→ PLUS(times(x,plus(y,times(s(z),0))),times(x,s(z)))
7:		TIMES(x,plus(y,s(z)))	→ TIMES(x,plus(y,times(s(z),0)))
8:		TIMES(x,plus(y,s(z)))	→ PLUS(y,times(s(z),0))
9:		TIMES(x,plus(y,s(z)))	→ TIMES(s(z),0)
10:		TIMES(x,plus(y,s(z)))	→ TIMES(x,s(z))
11:		TIMES(x,s(y))	→ PLUS(times(x,y),x)
12:		TIMES(x,s(y))	→ TIMES(x,y)
13:		PLUS(x,s(y))	→ PLUS(x,y)

The approximated dependency graph contains 2 SCCs: {13} and {7,10,12}.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(PLUS) = 2 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {7,10,12}. The constraints could not be solved.

Tyrolean Termination Tool (0.26 seconds) --- May 4, 2006